Conventional source code checkers include a source code analyzer for checking properties related to program (also described as “application program” hereinafter) behaviors meant by source code. Source code analyzers include a source code model checker for analyzing source code using model checking technique.
Behaviors of an application program expressed by source code means a series of program operation, instructed by a series of instructions described in source code. Properties related to these behaviors include a property of, if memory is dynamically allocated, reliably releasing the memory, and a property of, if an instruction in a program is executed, reliably executing the corresponding specific instruction sometime.
Model checking refers to, when specifications expressing properties to be checked and a target model for checking are input, judging whether or not the model has properties expressed by the specifications. An apparatus for performing model checking is called a model checker, and what describes a target model for checking is referred to as model description. A language for describing a model varies in many ways depending on a model checker. In a case of the SPIN model checker, for example, the language for describing a model is what is called Promela.
The SPIN model checker is a checker for checking whether or not a system modeled as a finite-state transition system exhaustively satisfies a checking expression described in a linear-time logical expression in full state search. The SPIN model checker is disclosed in The Model Checker Spin, G. J. Holzmann, IEEE Trans. on Software Engineering, Vol. 23, No. 5, pp. 279-295, May 1997, for example.
Source code model checking refers to model checking targeted for checking source code, a term used in contrast with hardware model checking, which is targeted for hardware such as a logical circuit.
Conventional source code checkers include those using a conversion table for translating source code into a language to be input to a model checker. The makeup is disclosed in U.S. patent applications No. 2001/0037492 and No. 2002/0100022, for example. FIG. 14 is a block diagram illustrating the makeup of the conventional source code checker described in No. 2001/0037492.
The model checker shown in FIG. 14, which is a conventional source code checker, inputs source code 1301 under checking from source code input unit 1302. Next, this source code checker composes a control flow graph according to source code 1301 accepted by source code input unit 1302, at source code conversion table generator 1303. Then, the source code checker generates source code conversion table 1304 that is a collection of parallel translation examples described in a corresponding model description language such as Promela, from the control flow graph, for each statement of source code 1301 under checking.
Next, model description generator 1305 converts source code 1301 into a model description language using parallel translation examples included in source code conversion table 1304. Specifications input unit 1307 delivers specifications 1308 to be checked describing specifications expressing properties of source code 1301 to be checked having been input, to model checker executing unit 1306. Then, model checker executing unit 1306 executes model checking using specifications 1308 supplied from specifications input unit 1307 and the model description generated by model description generator 1305, and outputs checking result 1309.
If source code conversion table 1304 automatically generated is undesirable for the user of the source code model checker, correcting means 1310 of the user needs to correct source code conversion table 1304 as appropriate. Such cases include one where source code 1301 under checking handles what is not included in the source code, such as communications with an external module. Source code conversion table generator 1303 often fails to present a correct translation example, which the user needs to supplement.
A model description language used for source code model checking (e.g. Promela) is different from a programming language for describing source code (e.g. C language) in expressive power. Specifically, some transition conditions can be described in a programming language, but not in a model description language. Accordingly, behaviors meant by source code can be essentially difficult to accurately translate into a model description language, and generating an appropriate source code conversion table is often difficult. Thus, a model description is not available that accurately reproduces behaviors meant by source code under checking, often resulting in inaccurate checking.
In detail, model checking is performed in the next procedure. That is, a labeled directed graph is generated according to a model description, and judgement is made whether or not the graph satisfies constraints meant by specifications expressed by a linear-time logical expression, for example. A linear-time logical expression is formed by adding a concept of time to a propositional logical expression, widely used when such as describing a state transition model formally.
A labeled directed graph is composed of a set of nodes and links. Each link represents relationship between two nodes, and a link connecting the nodes together has a direction. More specifically, a labeled directed graph has two nodes each corresponding to the origin and endpoint of a link, where each node has a label attached.
A labeled directed graph is regarded as a state transition diagram when each node of the labeled directed graph is regarded as a state; and movement from a node to another along the direction of the link, as a state transition. A label at each node is regarded as an event occurring in each state. Model checking judges whether or not a series of event occurrence satisfies constraints of given specifications.
However, a labeled directed graph is not provided with a transition condition. A transition condition is one for judging to which link (i.e. which node of the endpoint of a link) transition is to be made if plural links with a node as its origin are present. Absence of a transition condition means that a state corresponding to a node of which link is regarded as the next state is arbitrarily selectable if plural links are present. Model checking usually judges whether or not constraints of specifications under checking are violated, and thus the worst case is always selected for an arbitrarily selectable transition destination.
However, a state transition diagram expressing behaviors meant by source code is generally expressed by a labeled directed graph with a transition condition. For a conditional clause expressed by an ‘if’ statement, for example, a true or false value of the conditional expression determines a next state.
The above-described reason can cause the following problem. That is, literal translation involves essential difficulty between a model description language implicated by a labeled directed graph without a transition condition, and a general programming language implicated by a labeled directed graph with a transition condition. Further, the conventional method can make it difficult for the user of the checker to correct the source code conversion table.
In detail, the user of the checker, when correcting a source code conversion table, needs to understand a model description described in the conversion table. The user further needs to locate a part that does not accurately reflect behaviors of the application program meant by the source code, and needs to provide an alternative translation for such a part. Moreover, while considering so that model checking is appropriately performed for a part other than the source code under checking, the user needs to provide a model description complementing the part. These jobs can involve difficulty and complications even if the user is an expert on model checking.